Closes both acceptance criteria of #56 — though the second was already
satisfied, and the first was mis-scoped.

## Criterion 1 — template residue

The issue recorded *"5 `{{PLACEHOLDER}}` files + 8 `rsr-template-repo`
references"*. Re-measured: **8** files matched `{{...}}` and **21**
lines matched the template name — but most were **meta-references**:
files *describing* the debt, not carrying it.

Three would have been damaged by a naive search-and-replace:

| File | Why it must not be touched |
|---|---|
| `src/rust/src/eval.rs` | `"...add{{}} block"` is a Rust `format!`
**escape** — `{{}}` renders as a literal `{}`, naming the `add{}`
language construct. Working code. |
| `methodology.a2ml` | The token appears inside `reject-if-contains` —
the rule that *forbids* it. |
| `AFFIRMATION.adoc`, `docs/identity-fabric/` | Prose recording the
debt. |

**The genuine residue, now cleared:** `{{DEPS}}`,
`{{BUILD_OUTPUT_PATH}}`, `{{PACKAGE_NAME}}`, `{{LANG_STACK}}`,
`{{BUILD_CMD}}`, `{{TEST_CMD}}`, `{{MUST_INVARIANTS}}`,
`{{PROJECT_UNIQUE_STRENGTH}}` — plus four contractiles and the citation
guide whose **subject was still the template**. `Intentfile` asserted
*"This repository is the canonical template for Rhodium Standard
Repository compliance"*; `CITATIONS.adoc` credited *"Polymath, Hyper"*
for *"RSR-template-repo"* in all five citation formats.

## A worse class, found while fixing it

All three QUICKSTARTs documented commands that **do not exist** — `just
build`, `just test`, `just lint`, `just panic-scan`, `just setup-dev`,
`just build-release`, `just install`, `just run`, `just heal`, `just
setup`, `just uninstall`, `just stapeln-run` — asserted an
`$XDG_CONFIG_HOME/tangle/config.toml` the compiler never reads, and
carried a *"Multi-Instance Deployment"* section for what is a single
stateless binary.

Documentation that fails when followed is worse than none. Every command
now shown is verified to exist, and the worked example shows the
**real** output (8 `assertion passed` lines, exit 0) rather than the
template's invented `Tangle started successfully.`

## Criterion 2 — already satisfied by #78

`README.adoc` carries the correction and `AFFIRMATION.adoc` has
*"Erratum — 2026-07-21 / Correction 1 — the stack does not exist"*.

Worth noting: the criterion as worded — *"does the simplified diagram
supersede, or re-state, the nuance?"* — presupposed the stack was real.
**Both options were wrong.** `KRL → TangleIR → …` describes a dependency
that never existed (`TangleIR` appears in no source file in either
repo). It was withdrawn, not reconciled.

## Making the rule real

`methodology.a2ml` has always declared `reject-if-contains = [...,
"rsr-template-repo"]` — and **nothing enforced it**, which is precisely
how the contractiles stayed mis-instantiated. Adds
`scripts/check-rsr-instantiation.sh` (plus `just rsr-check` and a CI
step), using an explicit allowlist so meta-references and the Rust
escape aren't false-positived.

**Verified adversarially:**

| Attack | Caught |
|---|---|
| Reintroduce a `{{PLACEHOLDER}}` | ✅ |
| Claim to be `rsr-template-repo` | ✅ |
| Document a phantom `just` recipe | ✅ |
| Rust `format!` escape `add{{}}` | ✅ correctly **ignored** |

It earned itself immediately: on first run it flagged
`QUICKSTART-USER.adoc`, a file I had not inspected, with six phantom
recipes.

## Also

`AFFIRMATION.adoc` gains a dated **Erratum — 2026-07-29** (Corrections
3–5) recording the residue clearance, that the OCaml compiler is no
longer unbuilt (#87/#89 — the previous erratum's closing line said it
was), and that `==` is no longer list equality (#50/#87).

All gates pass locally: build, corpus, rsr-check, `must-check`,
`trust-verify`.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

Four of the five unparsed `conformance/valid/` programs — `v02_weave`,
`v08_crossing`, `v09_twist`, `v12_weave_expr` — use weave as a
**definition body**:

```tangle
def simple_crossing =
  weave strands a:Q, b:Q into
    (a > b)
  yield strands b:Q, a:Q
```

The grammar allowed weave only as a top-level statement, so all four
failed. Typed strands (`a:Q`) and `yield strands` were never the problem
— those already parsed. Only the **position** did.

## Why the expression form is the right fix, not a corpus edit

My first instinct was that the corpus was wrong, since
`spec/grammar.ebnf` also said statement. Then I checked what a weave
statement actually *does*:

```ocaml
(* eval.ml *)
| WeaveBlock _wb -> (env, None)          (* no-op *)

(* typecheck.ml *)
let _weave_ty = TTangle (input_boundary, output_boundary) in
gamma                                     (* type computed, then DISCARDED *)
```

**As a statement, weave is inert.** It binds nothing, produces nothing,
and its type is thrown away. The construct could be written but never
used. Binding it to a name is the only thing that makes it reachable —
which is precisely what the corpus assumed all along.

The statement form is kept, so this is **purely additive**.

## Scope — no proof implications

Weave is outside the mechanised core: **0 occurrences in
`proofs/Tangle.lean`, 0 in the TG-3 corpus**. So this touches no proof
obligation, and `Weave` joins the other non-core constructors in
`tg3_emit`'s explicit rejection branch rather than being translated.

Threaded through `ast` (new `Weave of weave_block`), `parser`
(`primary_expr`), `typecheck` (types as the `Tangle[A,B]` it denotes;
body checked in the strand context exactly as the statement form does),
`eval` (the body *is* the value), and `pretty` (re-parseable form).
`expr_calls` also traverses into a weave body — otherwise recursion
inside one would be invisible to the #91 fixpoint search.

## What this does NOT fix: `v11_add_block`

`add{ 1 + 2 + 3 }` is **not a missing parse rule**. It is the **Harvard
data sub-language**:

| | |
|---|---|
| own expression grammar | literals, vars, arithmetic, equality,
`&&`/`\|\|`/`!`, calls, `if/then/else` |
| own type system | Int, Float, Rational, Hex, Binary, Bool, String,
Symbolic |
| own environments | `Π`, with visibility rules |
| own typing judgement | `⊢_hd` |
| conversion layer | Embed / Unembed |
| calling | bidirectional with Tangle |

**288 lines of `FORMAL-SEMANTICS.md` across 12 sections.** That is a
feature, raised separately. It remains the single entry in the corpus
manifest's known-gap list.

## Results

| | before | after |
|---|---|---|
| conformance | 14/19 | **18/19** |
| corpus manifest known-unparsed | 5 | **1** |

(It reported a *fake* 3/19 before #89 fixed the runner.)

The ratchet in `check-corpus.sh` **demanded** the manifest update — it
failed the build with *"now parses — drop it from
CONFORMANCE_KNOWN_UNPARSED"* for each file. That is exactly what it was
built to do.

## Tests

- weave as a definition body (the conformance form)
- **TG-4 round-trip**: pretty-print then re-parse yields the same AST —
needed because I changed `pretty.ml`
- guard that the statement form still parses (the change is additive)

Full suite green, 0 failures; TG-3 still 1008/0. `spec/grammar.ebnf`
updated to match, with the rationale recorded.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

…th (#95)

Implements the #92 ruling across both engines — plus two bugs found
while verifying it.

## The rule

`T-Eq-Word` required both operands at the same width. Four ways that was
inconsistent with the language itself (evidence in #92):

- **`tComposeWord` already widens** to `max n m` — you could compose two
braids you were then forbidden to compare.
- **`~` accepted differing widths** and, since TG-7, evaluates through
the *same* `Braid_equiv.equiv`. Identical operands, identical answer,
one rejected by the typechecker.
- **`eqIdBraid`/`eqBraidId`** decide "is this braid trivial?" against
`identity : word 0`, so under the old rule they could only fire when the
braid was empty. The step relation had rules for a question the typing
rule forbade asking.
- **`braid_equiv.equiv` has no width parameter at all.**

Lean's `tEqWord` now takes `(n m)`; `infer`'s `.eq` case drops the `if n
= m`; OCaml `Eq` mirrors it. Match arms join on width for words and
still require exact agreement otherwise.

## The metatheory needed no patching

**Progress, Preservation, Determinism, TypeSafety, `infer_sound`,
`infer_complete` all still hold** — `lean Tangle.lean` reports **0
errors**, sorry/axiom gate passes.

`infer_sound`'s proof got *simpler*: with no `if n = m` there's no inner
`split` to case on. A restriction whose removal shortens the proof was
carrying no weight.

**TG-3 regenerated and kernel-checked: 496 obligations, 0 errors.** 46
flipped from `= none` to `= some .bool` — exactly the `identity ==
braid` shape that was unreachable before.

## Two bugs found while verifying

**1. Statement order.** `parse_file_recovering` did `stmts := prog @
!stmts` then `List.rev` on the flattened result. That reversal is
correct for an accumulator built by prepending *single items* (as
`diagnostics` is) — but whole **segments** were prepended, so every
program came out backwards:

```
def x = 5     parses to    def z = 7
def y = 6      ------->    def y = 6
def z = 7                  def x = 5
```

Any program whose statements depend on order died with *"Unbound
variable"*. **The test suites never caught it because they call
`Tangle.Parser.program` directly — only the CLI goes through the
recovering path.**

**2. A false assertion in `examples/trefoil.tangle`:**

```tangle
assert reversed == braid[s1, s1, s1]     # reversed = reverse(trefoil)
```

`reverse` reverses the word *and negates exponents*, yielding the
inverse braid. Verified by invariant: `writhe(trefoil) = 3`,
`writhe(reversed) = -3`, and writhe is invariant under the braid
relations — so they cannot be equal. The assertion had been wrong since
it was written; nothing ran the examples until #89. Corrected to
`braid[s1^-1, s1^-1, s1^-1]`, which passes.

## Result

| | before | after |
|---|---|---|
| examples evaluating | 2/7 | **7/7** |
| `lib/stdlib.tangle` | did not typecheck | **typechecks** |
| conformance | 18/19 | 18/19 (`v11` is the Harvard sub-language, #94) |

All seven examples are now in the corpus gate's must-run set, so none
can regress.

## ⚠ Trusted base — registered as A-TG-92.1

The embedding **Bₙ ↪ Bₙ₊₁** that justifies cross-width comparison is
standard mathematics, but it is **asserted in prose, not mechanised** —
no Lean lemma states it.

What *is* machine-checked: that the metatheory holds under the widened
rule, and that OCaml `infer_expr` still agrees with Lean `infer` on the
corpus. That distinction is recorded in `ASSUMPTIONS.md` rather than
left implicit.

## Tests

6 new typecheck cases, including **two negatives** — mismatched *kinds*
still rejected, match arms of different kinds still rejected — so
widening cannot quietly become "anything compares to anything". Three
`test_check` cases repointed at an error that is still an error (and an
assertion helper left unused by the change was put back to work rather
than deleted).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>